Nuprl Definition : combine-ecl-tuples 0,22

combine-ecl-tuples(A;B;f;g)
== let Ta,ksa,ia,ga,ha,aa,ae = A in 
== let Tb,ksb,ib,gb,hb,ab,be = B in 
== <(TaTb)
== ,(ksa @ ksb)
== ,<ia,ib>
== ,(k',s,v,x. <if deq-member(KindDeq;k';ksa) ga(k',s,v,1of(x)) else 1of(x) fi
== ,(k',s,v,x,if deq-member(KindDeq;k';ksb ha(0,1of(x)) gb(k',s,v,2of(x)) else 2of(x) fi>)
== ,(n,xf((m.ha(m,1of(x))),m.hb(m,2of(x)),n))
== ,(n,k',s,v,xg
== ,(n,k',s,v,x(if deq-member(KindDeq;k';ksa) aa(n,k',s,v,1of(x)) else false fi
== ,(n,k',s,v,x,if deq-member(KindDeq;k';ksb) ha(0,1of(x))  ab(n,k',s,v,2of(x))
== ,(n,k',s,v,x. ,else false fi))
== ,merge(ae;be)> 
latex


Definitionslet a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), as @ bs, if b t else f fi, deq-member(eq;x;L), KindDeq, p  q, 1of(t), 2of(t), false, merge(as;bs)
FDL editor aliasescombine-ecl-tuples

origin